pre{-}init{-}p(${\it es}$; $i$; ${\it ds}$; ${\it init}$; $P$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$($\uparrow$($P$($\lambda$$x$.${\it init}$($x$)?$\cdot$))) $\Rightarrow$ ($\exists$$e$:E. (loc($e$) = $i$))